es:ES, Ack, Req:(E), f:({e:E| Ack(e)} {e:E| Req(e)} ).
e.f(e) is c< preserving on e.Ack(e)
 (e, e':{e:E| Ack(e)} . (e' c e)  (e < e'))
 (e, e':{e:E| Req(e)} . (e' c e)  (e < e'))
 (e, e':{e:E| Req(e)} . (e < e')  (a:{e:E| Ack(e)} . ((e < a) & (a < e'))))
 (e:E. Req(e)  (a:E. Ack(a)  e c a  e c f(a))) 

latex

Definitions

e c e', x:A. B(x), True, T, P  Q, x:AB(x), SqStable(P), x:A  B(x), P & Q, x:A. B(x), Type, , e < e', {T}, WellFnd{i}(A;x,y.R(x;y)), t.1, s = t, False, A, left + right, P  Q, Dec(P), b, ES, a.f(a) is c< preserving on e.P(e), EqDecider(T), Unit, IdLnk, Id, EOrderAxioms(E; pred?; info), EState(T), Knd, kindcase(k; a.f(a); l,t.g(l;t) ), Msg(M), type List, , , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), r  s, , constant_function(f;A;B), Top, let x,y = A in B(x;y), e loc e' , (e <loc e'), x.A(x), x. t(x), pred!(e;e'), SWellFounded(R(x;y)), Void, x:A.B(x), S  T, suptype(S; T), first(e), loc(e), <a, b>, x,y. t(x;y), kind(e), f(a), x(s), E, {x:A| B(x)} , t  T, (e < e')

Lemmas

es-causle weakening, es-causl transitivity2, es-causl irreflexivity, deq wf, EOrderAxioms wf, Id wf, kind wf, loc wf, Msg wf, nat wf, val-axiom wf, cless wf, qle wf, bool wf, rationals wf, Knd wf, kindcase wf, IdLnk wf, EState wf, constant function wf, assert wf, first wf, top wf, unit wf, event system wf, es-E wf, causal-order-preserving wf, not wf, es-causl-wellfnd, es-le-causle, es-causle-le, es-causl wf, es-causle wf, sq stable from decidable, decidable es-causle